Dynamic model checking has been shown to advantageously provide the direct verification of concurrent programs written in contemporary programming languages such as C and Java, by systematically executing a program in its target environment under different thread schedules (interleavings). Since such techniques execute the program itself rather than a model, they do not produce bogus errors when verifying safety properties, such as local assertions.
For verifying terminating programs—unless context-bounding is imposed—these methods are also complete (i.e., do not miss any real error). However, explicitly enumerating thread interleavings is “expensive” since the number of interleavings may be very large.
Dynamic partial order reduction (DPOR) has been used in to “prune away” redundant thread interleaving. For each (Mazurkiewicz) trace equivalence class of interleavings, if a representative has been checked, the remaining ones are regarded as redundant. However, DPOR only removes redundant interleavings within each equivalence class, it does not help when an equivalence class itself is redundant, e.g., with respect to a correctness property. In such cases, a property specific reduction is required to prune away the redundant equivalence classes. Property specific reduction can be achieved by symbolic methods using an underlying satisfiability (SAT or SMT) solver. As used herein, SAT formula denotes a formula either in Boolean logic or in a quantifier-free first-order logic while SAT solver denotes a decision procedure of SAT formulas.
With symbolic methods, verification is often posed as a satisfiability problem such that the SAT formula is satisfiable if there exists an interleaving execution of the program that violates the property. The reduction happens inside the SAT solver through the addition of learned clauses derived by conflict analysis. However, a disadvantage of SAT-based symbolic analysis is that it does not scale well to the entire program, because the cost of checking all possible program executions is often too high.